(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(a, f(b, x)) → f(b, f(a, x))
f(b, f(c, x)) → f(c, f(b, x))
f(c, f(a, x)) → f(a, f(c, x))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(a, f(b, z0)) → c1(F(b, f(a, z0)), F(a, z0))
F(b, f(c, z0)) → c2(F(c, f(b, z0)), F(b, z0))
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
S tuples:
F(a, f(b, z0)) → c1(F(b, f(a, z0)), F(a, z0))
F(b, f(c, z0)) → c2(F(c, f(b, z0)), F(b, z0))
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c3
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a,
f(
b,
z0)) →
c1(
F(
b,
f(
a,
z0)),
F(
a,
z0)) by
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, x0)) → c1
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(b, f(c, z0)) → c2(F(c, f(b, z0)), F(b, z0))
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, x0)) → c1
S tuples:
F(b, f(c, z0)) → c2(F(c, f(b, z0)), F(b, z0))
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, x0)) → c1
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c3, c1, c1
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(a, f(b, x0)) → c1
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(b, f(c, z0)) → c2(F(c, f(b, z0)), F(b, z0))
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
S tuples:
F(b, f(c, z0)) → c2(F(c, f(b, z0)), F(b, z0))
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c3, c1
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
b,
f(
c,
z0)) →
c2(
F(
c,
f(
b,
z0)),
F(
b,
z0)) by
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(b, f(c, x0)) → c2
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(b, f(c, x0)) → c2
S tuples:
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(b, f(c, x0)) → c2
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c3, c1, c2, c2
(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(b, f(c, x0)) → c2
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
S tuples:
F(c, f(a, z0)) → c3(F(a, f(c, z0)), F(c, z0))
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c3, c1, c2
(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
c,
f(
a,
z0)) →
c3(
F(
a,
f(
c,
z0)),
F(
c,
z0)) by
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(c, f(a, x0)) → c3
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(c, f(a, x0)) → c3
S tuples:
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(c, f(a, x0)) → c3
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c3, c3
(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(c, f(a, x0)) → c3
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
S tuples:
F(a, f(b, f(b, z0))) → c1(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c3
(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a,
f(
b,
f(
b,
z0))) →
c1(
F(
b,
f(
b,
f(
a,
z0))),
F(
a,
f(
b,
z0))) by
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, x0))) → c1
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, x0))) → c1
S tuples:
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, x0))) → c1
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c3, c1, c1
(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(a, f(b, f(b, x0))) → c1
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
S tuples:
F(b, f(c, f(c, z0))) → c2(F(c, f(c, f(b, z0))), F(b, f(c, z0)))
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c3, c1
(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
b,
f(
c,
f(
c,
z0))) →
c2(
F(
c,
f(
c,
f(
b,
z0))),
F(
b,
f(
c,
z0))) by
F(b, f(c, f(c, f(c, z0)))) → c2(F(c, f(c, f(c, f(b, z0)))), F(b, f(c, f(c, z0))))
F(b, f(c, f(c, x0))) → c2
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(b, f(c, f(c, f(c, z0)))) → c2(F(c, f(c, f(c, f(b, z0)))), F(b, f(c, f(c, z0))))
F(b, f(c, f(c, x0))) → c2
S tuples:
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(b, f(c, f(c, f(c, z0)))) → c2(F(c, f(c, f(c, f(b, z0)))), F(b, f(c, f(c, z0))))
F(b, f(c, f(c, x0))) → c2
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c3, c1, c2, c2
(21) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(b, f(c, f(c, x0))) → c2
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(b, f(c, f(c, f(c, z0)))) → c2(F(c, f(c, f(c, f(b, z0)))), F(b, f(c, f(c, z0))))
S tuples:
F(c, f(a, f(a, z0))) → c3(F(a, f(a, f(c, z0))), F(c, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(b, f(c, f(c, f(c, z0)))) → c2(F(c, f(c, f(c, f(b, z0)))), F(b, f(c, f(c, z0))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c3, c1, c2
(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
c,
f(
a,
f(
a,
z0))) →
c3(
F(
a,
f(
a,
f(
c,
z0))),
F(
c,
f(
a,
z0))) by
F(c, f(a, f(a, f(a, z0)))) → c3(F(a, f(a, f(a, f(c, z0)))), F(c, f(a, f(a, z0))))
F(c, f(a, f(a, x0))) → c3
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(b, f(c, f(c, f(c, z0)))) → c2(F(c, f(c, f(c, f(b, z0)))), F(b, f(c, f(c, z0))))
F(c, f(a, f(a, f(a, z0)))) → c3(F(a, f(a, f(a, f(c, z0)))), F(c, f(a, f(a, z0))))
F(c, f(a, f(a, x0))) → c3
S tuples:
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(b, f(c, f(c, f(c, z0)))) → c2(F(c, f(c, f(c, f(b, z0)))), F(b, f(c, f(c, z0))))
F(c, f(a, f(a, f(a, z0)))) → c3(F(a, f(a, f(a, f(c, z0)))), F(c, f(a, f(a, z0))))
F(c, f(a, f(a, x0))) → c3
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c3, c3
(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(c, f(a, f(a, x0))) → c3
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(b, f(a, z0))
f(b, f(c, z0)) → f(c, f(b, z0))
f(c, f(a, z0)) → f(a, f(c, z0))
Tuples:
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(b, f(c, f(c, f(c, z0)))) → c2(F(c, f(c, f(c, f(b, z0)))), F(b, f(c, f(c, z0))))
F(c, f(a, f(a, f(a, z0)))) → c3(F(a, f(a, f(a, f(c, z0)))), F(c, f(a, f(a, z0))))
S tuples:
F(a, f(b, f(b, f(b, z0)))) → c1(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(b, f(c, f(c, f(c, z0)))) → c2(F(c, f(c, f(c, f(b, z0)))), F(b, f(c, f(c, z0))))
F(c, f(a, f(a, f(a, z0)))) → c3(F(a, f(a, f(a, f(c, z0)))), F(c, f(a, f(a, z0))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c3
(27) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
a0() → 0
b0() → 0
c0() → 0
f0(0, 0) → 1
(28) BOUNDS(O(1), O(n^1))